\begin{tabbing}
$\forall$${\it es}$:ES, $i$:Id, $P$:(discrete state@$i$$\rightarrow\mathbb{P}$).
\\[0ex]@$i$ stable ${\it state}$.$P$(${\it state}$)  
\\[0ex]$\Rightarrow$ \=$\forall$$e$@$i$.\+
\\[0ex]$P$((discrete state after $e$)) $\Rightarrow$ ($\forall$${\it e'}$:E. ($e$ $<$loc ${\it e'}$) $\Rightarrow$ $P$((discrete state when ${\it e'}$)))
\-
\end{tabbing}